A || B
== if Rplus?(A) Rplus-left(A) || B & Rplus-right(A) || B
== i; Rplus?(B) A || Rplus-left(B) & A || Rplus-right(B)
== i; Rnone?(A) True
== i; Rnone?(B) True
== i; R-loc(A) = R-loc(B)
== i; Rds(A) || Rds(B) & Rda(A) || Rda(B)
== i; & if R-base-domain(A) = R-base-domain(B) A = B
== i; & else R-frame-compat(A;B) & R-frame-compat(B;A) fi
== else R-interface-compat(A;B) & R-interface-compat(B;A) fi
(recursive) 

latex

---

clarification:

R-compat{i:l}
R-compat(A; B)
== if Rplus?(A) R-compat{i:l}(Rplus-left(A); B) & R-compat{i:l}(Rplus-right(A); B)
== i; Rplus?(B) R-compat{i:l}(A; Rplus-left(B)) & R-compat{i:l}(A; Rplus-right(B))
== i; Rnone?(A) True
== i; Rnone?(B) True
== i; R-loc(A) = R-loc(B)
== i; fpf-compatible(Id; x.Type{i}; IdDeq; Rds(A); Rds(B))
== i; & fpf-compatible(Knd; x.Type{i}; KindDeq; Rda(A); Rda(B))
== i; & if R-base-domain(A) = R-base-domain(B) A = B  es_realizer{i:l}
== i; & else R-frame-compat(A;B) & R-frame-compat(B;A) fi
== else R-interface-compat(A;B) & R-interface-compat(B;A) fi
(recursive) 

latex

Definitions	Y, x.A(x), Rplus?(x1), Rplus-left(x1), f(a), Rplus-right(x1), Rnone?(x1), True, a = b, R-loc(R), Id, IdDeq, Rds(R), f || g, Knd, Type, KindDeq, Rda(R), if b t else f fi, p = q, R-base-domain(R), s = t, Realizer, R-frame-compat(A;B), P & Q, R-interface-compat(A;B)
FDL editor aliases	R-compat